ds:(IdType), da:(IdKndType), A, B:Type, X:Interface(ds;da;A), Y:Interface(ds;da;B).
interface-union(X;Y)  Interface(ds;da;A + B) 

latex

Definitions

LocKnd, t  T, Id, x:A. B(x), hasloc(k;i), b, Knd, {x:A| B(x)} , Top, left + right, x:AB(x), f(a), x,y. t(x;y), let i,k:LocKnd = ik in P(i;k), x.A(x), x. t(x), a:A fp B(a), (x  l), fpf-domain(f), as @ bs, <a, b>, type List, x:A  B(x), , interface-union(X;Y), Interface(ds;da;A), Type, A, s = t, a < b, b, , locknd-deq(), x  dom(f), P  Q, P & Q, P  Q, Unit, if b then t else f fi , f(x), inr x , inl x , case b of inl(x) => s(x) | inr(y) => t(y), P  Q, False, P  Q

Lemmas

member append, member-fpf-dom, fpf-ap wf, eqtt to assert, iff transitivity, eqff to assert, assert of bnot, fpf-dom wf, locknd-deq wf, bool wf, bnot wf, not wf, append wf, fpf-domain wf, l member wf, fpf-trivial-subtype-top, locknd-spread wf2, top wf, Knd wf, assert wf, hasloc wf, Id wf, LocKnd wf